■
Artificial Intelligent Froie3fc-*HI£ ani K.{T Computation renter
Wenc &i--The Prcofsbcsker
by
Pail Abraham
.... . ' •
-January £&, ipol
JiBSTMGS
The Frt:cf'ih^tVi r er ifi £ heurle tic-ally tri«itei cCB^putai? pro-
gram for checking ira^matita! proofs ? w.'.th tb* ftheairtrtE of text-
tccvc pp^pffl &g it* ultimate e<*al, :ft tone frusta, from esa* P* cc "?
step jrii-»n to it. a. *orT£sponJin£ negusn-e of fcrrai Etepe, if
pc.adibla. H peaor&a tha current ttate of the prcof in fcha forra
of itfat It -56 s=uTJ.'JiJ.en*. tc prtve. There are two Logical Pul*S rf
iaferenaa; »c*™ power* and iisasrlion (if it i* sufficient to
prove P N 5^ A i*. a liheorein, tlien it is sufficient to prove A
iiip^es F)* The peuniBPible fnvwai Ptepa ■■.rilJde these rules of
infer eu-e as weii as provision fci hawSling definitions, icnaa,
cB-l^tiiatlons, and revision ec previous state?. A? of now, mast
of the fortnalipnt, o.?i* pjcsr&wip»3 an* partially debugged, bat the
heurlatle &Epe-;tr have yet tc. be pro^raimnii*
* v
■£<-
TABLE OF CCNTEKIS
i ?utpofe arid pttLloAaphy ■ * * * * * r * *' * ' "
II OffsanasatJon of the ?rcof checker 7
III Logical Po-JErfatloBB of the Proof rtwdur - * • * ■ 13
IV Th* Poasitl* Froor S:;e*s in th-s Proof eh#a«ep - - 1?
7 Current Sfcatug and Future Plans
3
PI
-3-
^JUPOSE AND PHILOSCPHI
A proofs heeler la a computer program v:hlch checks watheriiatical
proof* to- eeo if they ars correal;, k TnatheEr-atJ ral proof is a sym-
bolic express! on f antf ao can be used aa input data for a "f^rnpitsr
program vjritfcan in a syuibol-Gr.a.nipul&tlng l&nguage , Now if a
proposed £roof has been sufficiently formalized, it can be the aired
by a n*mple set of rules j but if che proof is of the sort that
appears in most mathematics textbooks t the checking pro^c-dsra siyat
be ft* Irene 3 y elaborate and even then cannot be guaranteed to worfc
all the time.: Crhfi~! r .ino; textbook proofs ia the ultimate goal of
tne Proof checker project, even thoarh it pirobably will not be
reached, this goal Mli est [>hs direct if n of thete effort?-; how
fa>? they go rentf'ns to be seen* Some programs have already been
ch-C-kid out; rrttiiy regain to be written* ha of this writing two
el^w^fjfcft^y formal "proofs h.ive been chocked.:
h n -inter of the ideas presumed in this paper arose from
suggestions made by £ohn McCarthy? however., the vIoyIhj expressed
hoi.-e are not ne-ieesarily in a^re e [Dent v/ith McCarthy's.,
?herc are two difficulties that arise in demising a procedure
for checking ccjctbooln p-rcofiK First, the proof 3. are written in
English \ se-eorjd, they ars ambiguous, inforital, and .full of gapGr
I am not at present planning to deal with the first problem? though
it 1b interesting, it is irrelevant to the main purpose of the
Proof checks project* Therefore, 1 will afisutw that the proofs
;:hi.ch I wild like the Proof checker to sparine Mill be presented
in a foraialised and stylised language, but one which makes no
attempt? to clarify the logical defects of the English original
from which thej are taken* The Pyoof^hej^er will have to correct
these defects and check the resulting formal proof at the aame time*
Essentially* the Proof ohec iter works by talcing each step that
it it given and gens rating fror it a aequense or formal steps L
Thus the proof given to it really serve a as a set: of hints on how
to construct a formal pre of of the theorem at hand. The Proof-
checker tnurt be something of a proof inventory t&v it mu&t among
-it-
■
■
, other things be able lo handle strips labelled as "obvlouo*. As
the capabilities of the Proof checker increase, It i?il 1 got better
and toot tor at proving nen theorem In fact, we ttay view the job
of the Pi?oof checker to be to invent proofs, given a est of hints:
in the two extreme capes, the hlnta ara either nonexistent or are
all the utepe of a rorm&'L issd proof..
l.'e may consider tha problem from the viewpoint cf checking
:iEthorta for gene rat ins proofs, lie., seeing; if a proposed Fi*?thod
of proof generation gsnevatas a p^'oof of a desired theorem. Tha
two viewpoint** are equivalent; tw a technique which will utilire
Mnt? is 5irzply a proof Generator with an jnput., Further, tha
Proof checker H-isfc be able to bkl!£3 use of information on ehat the
(ceDbsia of a cai'. af.n c^a=;? of goalie expressions are legitimate
proofs Such a piece of InVori-^ilon is a n-eta theorem, In order
for any proof -checking ay stem to lit i lice rcetefchsorems, they ia<ist
bo built Into its etr J:?tiire^ fn the Proof checker , rce t a theorems
ciay be adder! without- ?hans£r£ * h* overall pattern of operation?
aarentij:,iy P they are added tc the list of perraiselble proof atepra f
so thay they act like addltif^ai rules o^ inference (vhieh, inieod,
they are U
The Heuristic A pproach 311S ii elatgd Work
The Froofcbeeker win make extensive use of heuristic methods
■:":;. ti.;-hi-.3qu^3 . "h:!e is rii-cfizsary became a a tr^.i T.'-.s.f.- r.'.'^-d 3-p-j,rch
through tha space of ooruv-tctions between snese salve hints would in-
volve an impossibly l*r£. amount of computation, One scheme which
I hop± will be useful h?,e will be the ,: Oer.&rsl Problem Solving
System ! ' of fleuc-11 and E .uz-tu This system has already been ured in
solving problems in trjgonoraetry, ele inert try algebra, and logic.
The chief feature of '.tie system is Its separation of probl&ra content
from proMem- solving rechnJque * jtt mattes use of two principal
heuristic a: meanF-erda ane^-ysls, which invo]vea knowing what
rrsthods of attack a]? epproprjate to particular situations, and
planning which iaveivea consideration of an abstraction of Che
-5-
■
problem tt hand* Closely r^ated to the fanning heuristic 1& the
heuristic of modele as Uf.ed by Oelorntsr.. TiIe he- i :iriEtic y for tfcs
case of plane goetSiefcr:/ r involves drawing figures and checking there
to pee what relationships hold between tarloup line aecnsntg,
anglee , etc*
There is a r>e&ei£flan:<e between the pole of hints- in the
Proofchecker alftd the rely of advice in McCarthy r e Advice Tales r
achem^ in each fere, hfj i^nt a DiaohJ.se to nahe use of pieces of
information given to It r? rorj an external source in ord^r to so^ve
a problew. In thr* case of . ty.a Proof checker* the structure of the
*advi<V r Kiak^o it raucfc e.ifJer to rtct armies how tc use it t
Problem ^tflains
The * , roofchecrk , e-r will not he tied to any particular area of"
[jia:--heinatics , although 1 espeit to work mainly on abstract algebra
at fi:?Efc, Tjhe Proof checker* like the mat hcrcaM clan, is Interidel
to bo a general -pLirprpe device* Her s. given problem doo&ln, it
will have relevant thecreiae, heuiMsti£,s 4 a>id tiodel-mkinc rae cho-
rd yfc. store;! in its ra^ory* Actually* it would be useful if the
Pi?oof shocker could be aiiari: of ili_ the theo rents It had ever
prove i n , though it udc,hi have le;sp ready a^eas to those from
different dom^Inf., The difficulty here Is that thara ainply
isn ! t enough took iii the cemputerj as things stand n^tt, for the
addifcio-nal t^eor-ems.
One poaalble ar^a ef application, thojgn ad wit ted ly soisewhat
futuristic, is to bhc uftseiwut of lai-f* ey&t*e?fl* The present way
that one checks r-uch a £;yst-5GJ to pee If St crorfre ia to p^e^ent it
tilth a wide vsrie.fcy *>f inputs representing both typical and extreme
taped, and see If the proper output results^ However, it often
happens that thii ic^thoci simply dca&ii't ^or!^; the system falls
under podes unanticipated combination cf circuraatari^ag which nswr
3i;Curred in the tes* •- af pe t One i/ey tc check out such a system,
however, la to pi- eve that it" worlr^ « Such a proof 4 of course t would
be inpoeeible for a hufcn to Construct fc*r a system of aven aSld
coup laxity; but a machine night b* £bis to eonatm-t such a proof,
iiFiinfl as h*n^s the £t scrip!: I on of tbs- functions and intondsd rao3e
of operations i?f various floiaponan^a and subcomponents of tha
syjifcett* And in a prcof atfcaEipt, one rci^h^ ccrae up a'th g.'
cO'^^terexampI-3 ar.d pcssibi/ ev T e:i sii^jzeifc e rer^dy*
-7-
'GitfAfflZA^TOH OF THE PROOF^'HECKER
The Proof checker is organized 'nfco ti:e constellations of
programs? Wo^hoe. and Verify. In a> Iltion to tho data interna]
to these programs., Clwre if a list a? theorem, a 13 at of defi-
nitions* and a J % *t o? ,lo£ltUiat3 prwif .*tep3, Tlw theorem list
and definition li?it may be a treated with time. verify will
accept a proposad fonral pr;of step and tietermins If it is correct i
if ths 3 tap ie cornet, Verify will d:> ths necessary updating of
fche state of the universe, Method will tie t ermine what th<2 next
step should be; it will make its a of nhe hints given as input in
finding this step. The steps tehich Verify Bill accept must be Jn
Bb&ndsrdlzed form? thus , all of the heuristics ara in the province?
of Method, though Verify will hurnJl: updating in such £. teay as to
rea^e the- u.eo of hourie bice easy*
The current stats of the proof 13 recorded in the form of
what it is sufficient to p;?ovo* We will call this expression the
CLifficiansy, i,e., at each stage It iu sufficient to piovs the
ftufficlency* Then Ir/tially, tho sufficiency its the theorem wa
uistt to prove; arei Nhen the sufficiency hsa been reduced to T
{truth), we know vs have proved fchs theorem* Wb nay record the
tuff icier cy at various stages of ths proof sncl refer bncif to it
later, oo that If r,s conduct an unsuc easeful aubprobleBa exploration,
ve :3an return to E.n earlier siabproblerc ivithznit havir.a to repeat the
Initial stops of tbo proof*
This particular foiw of recording - ne iurrent situation is con-
venient because of the uids variety of logical s true fur as which may
appear in a theorem or in it& p?ocf* "0 use a list of hypotheses
and conclusions would ba aukw&rd, for instance, In handling an if-
and -only- if thaorena, unless ilr were to be broken doe:n into two
separate theorem* • Yet Eu^h theorem;? are often proved by a sequence
of bi conditionals > and this natural sequence can be retained in the
sufficiency forir-oiaticm of the proofs Further more, this formulation
aaliK-a backwards proofs quite easy to handle, and they ara per hips
the moat nature! kind, Afc the tf&iae time, It x is possible by using
certain logical taut qloEi.es- to icake forward proofs; and the
TqaC'tilnsry for hanlllng Such ^roofE oan b-2 fc.il Ifc into Mofchod irt
sueh 4 WE.y that the u&er need not be a;sa.ve of the few complications
that this entails-
■■ ■ • . ■ . . - .
The Theodora Llet
The Pro of checker in endowed with an initial get of theorems
which are placed on a tli^orem 11a t„ ani each newly proved theorem
Is added to this 15 at. t^mraas proved during the course of pravinE
a theorem are also added to Ihis list. When-aver a theorem ia
referred to In a proofs it. is btoucht to the head of the theorem
list j so that frequently u^ed thacretifc are ennily ac c ass Ibis «
Each theorem consists of a nam?, a list of variables t and £
forjtu Whenever the theorem is used In a proof, it Is referred to
by narcsj the va^ifcibles designate those elen>snbs In the forci which
lt.:^ b^ substituted for* We z?s.y think of the variables as
designating an^.vei-sal iiutntlfiers which I implicitly precede the
forra so as to convert It to a th^orew in the ordinary senao. The
form is the actual statement of the theorss; no inhjarsnt res trl-t ions
are placed upon its foriaat, though for any problem domain, the
format will be specified.
The Cefl r ltlon List
The Proof che; Iter aim h&e available to it a list of definitions,
A proof r.ay bs interrupted at amy point to raaUe a new definition*
A definition is a Imply an abbreviation, with provision for sub-
otltuting- for certain variables within it a Each definition consists,
of two r-ames, a list of variables , and a form. The reference nacig
Is U&&d when, we refer to the definition ir a proof step, and the
Internal na^a is the one actually recorded in the sufficiency and
in any theorems or. the theorem list in which the definition ia
used^ The form ard variables operate in the sane way as the form
and variables in £ theorem. DefinllimiS, like theorems, are
arranged ao that recently used definitions appe&r at the head
the list.
■ ■ ■
Th.-i Need for Two Faroes
1
We need two narca-B in a dof Jnltion because etheruiae we way
accidentally assl^i to & definition a re revenue nrne whith already
I133 a meaning; and then >y riiklr^ use of the definition, ws nay
make e false atep »-:hith vrill p?>hf ^'r^rf-.U Ar, —iewdIs 7? ill
illustrate fetis danger* jiftpMe now that we have cii]y one name
aepioclafci;d wiC-h & definition* Let ue define AJ!D with varieties
X and li as {NOT, (OR.. X ? V? > n Tbtia AKD iq the raws, Ol, Y) it the
;lrt of variables, and ()3GT, {HR r a, ")) is ths fory& T Sew uuppose
Fiv^t ue h&ve as theorem (HOP, (OR. t, T)1, Shan ths theorem is
the original s uff iciescy, By ualng the d«fini felon * we may then
get a? sufficiency (AND, T. T); and by other Fjaara we loay reduce
thin to !?, ThU3 ws HOUL(i have somehow prevented froti: entering the
AJ3D Into the, Buffl&iency li! the above example, we would not have
bean sblu to carry out the proof. If an Internal natsa- say GOOOJ,
hat. been entered Jn p'.ise of AMD, we would have had as sufficiency
{GoGO^, ?, ?), which won! id be unprovable a 3 nee GO003 hag no Vrr?:"^
propel tl^y d
In jjensrLx.lj too u.i-e the raferencs n&i3ie when tie refer to & defi-
nition in a proof, bv.b the internal n&ma it the one actually re^oi-der
In the sufficiency. The Verify prcgrarc handles the "substitution of
■:ha internal nafl^ for th* reference mrae automat} eally,, Hhrr in-
ternal EfiiKto ic a newly" ^enar^ted aym'jol which can be guaranteed not
to have baen uaocJ for anything bsftre; the progrs-7?! which creates
i:ur.h eynbola lit l£$& is c-ajled Usrioyn, The symbols, it gens re. tee are
of the ft.ria Gxxxk, vrht.ra tha j: r s a^G d^cir.ial digits ^
Etedafinltion
It 3a possible to redefine a term 5/tr. though. It ha& previously
been defined, Itti-on ws cic thia t how-aver , vo lost the ability to
refer to the previous definition, This is hacausa whar. me eearGh
the definition JUrt for the reference riaise, wa will always come to
th^ later deficit len fir&t; and ws can ae^e-."^ a definition in a
proof step only through, ite reference name^ This le as one wo aid
:ika It to bai for St permits -^ to- make teTRporary definition?
-3.0-
of tense: without presr^diia ths later us?e of ths^e tortus for othar
purposes. The interna; 1 . r.aiTi^r of tho auctee-alvB definitions will
remain tniquey £o thr*re la no 3«n£er of ronfislori,
Often, f.n a he uric tin proof, tfe toil J Bake steps tshloh, rihila
correct, don't help to prove the Lheo^eig. Sir±«e sueh steps may
actually lead us to a r} tuition uhere ths suffis'^ncy la a fal-
sity {&r*d he/ite t&iprovafcle ) , we emefc have a May to e° bash to
pr-evtoiia suf fiajenoies.. At th*? same- tljae^ wq ^o^ h t want to fcssep
all previous Buffi^innujes, because it rjay talre up too igjoh rocra.
Therefore, there are tifc ways in which we nay nave past
sufficiencies..
BevertiRg
YJhen We il£tre a "tap, *ie nay request that tfc-j ^ast sufficiency
be preserved^ V't ns; 17 gi-ln R<33 eg 5 to :S t t-y reverting one or more
times, depending on how fp7 a] 0x45 va have Lioved subasfrjientlj .
Tr.ere It a parameter^ set by Wa^hoA, which tella Verify whether
or net to preserve ths most recant tuff ivis-nay,
Tt.a list of FjL T e_a_ejryed- jkib problerciE.
The reverting p^oc^dturji is no-: aj^uafce irhfcjj we wish to bail:
up several step?*, move ciff in aiiothar direction, and then, after
the r-ew exploration proves feasible, return to frh^re tje started.
It 1e inadequate be^auflfc th* starting point lies on a different
branih of the explorer Uw tree. ;{n order to handle this, there
Is provision for naming the eurri-n!: sufficiency at any tlras find
storing It on a list of auhproblero to be preserved. At any point,,
we mey reattach it if we: *j±fih„ We may also r-cmeva any a off id en-.: y
from the ltat of preserved QubptPOblenSr The items on the list or?
preserved aubproblenfi are then aoceaiad by their narae . When tha
theorem at hand h&a be*u proved, the list of preserved subproblems
If eL-t-onaeic&lly Glfi&rad,
-11-
Ea*.-h tyi» or proof etcp Is 1 rap**j*ent*d bjr & program which
taker ths parameters of the step as 'r.pul., updates Khatsye? needs
to bfj u-jduttd, and £.-v^ at output" T or 1'. d op 3-; lino; on Heather
or not she proof otap 1b correct. tfrtati (■■wis tr,sy toe incerpovatid
into ttto system If they ire sat up a& pace of etepaj crdlnsrilyj
they will tel:-s t;ie aaff.'^enay at as input , test it or a gutajt-
ppeefllon of L.t for a Et&:*tiful£r prcptrty, ar^l rberi trEnafariE It
in acta* uay L ]*q.' 2 list ante, £ 1o£I~el elc^lifijtUioR program would
correspond t-o b jestathsoreEj ru;l"! a pro^sa racjj.d red^c the
sufficiency to a ei;:^1#:? tuJ: logic ttlJv eq;uI T , ajLant- ibrci. The
actual raatatheoron ts?uirt be £hat Mis rssi;!: of t-lmplification is
*n a very case lo^jfc&Uy a^eivalsftfe to vha original, forra.
?»- j- V' erj.fy ?| 1 oc;j^m
Tb/i Verify vTrogr&S] . tp we hat;c po^n^.i out, ciitckB each
successive ftsp of the proof, and perfoi^ui: various k^nda of up-
dating* Before exEBSiiaine any eteps, it etijigns internal t:aro5£ fcc
f..".1 the variables p.o as to avcad &onfXi<strr i-;Jth preuto-jsly aBPlgned
Ckan?J^i: L Thereafter* when v^riLbl^a are referred -to fey their
ffcK&F, Verify raplAasn 1;h#BS n£Pi33 with Lhj internal names jjn the
eteps* of Hie proof., V;i-:e ir.iithtd nea-i no : e T jen be autare of the
existence of thoce iriti"ijal ns^ee*. UFarllv also asts tha 3Jfficic;niy
inJilall.y to bo zht theorem wt v:ieh to prt^i; wh^n thfi khsorarn h^a
been proved , V*fify pln.cfc- it s.t the hear? t>£ the theorem list.
Verify repeatedly calls on Hstho-l to ppodL.'.e a prcof etep fl Each
pt-ooi" slop it in-Heated b*y the r-fi" 1 ^ of a p;^£rari> sr.d- a get of argu-
ments for tht,t p?cgr&n; , Verify ^hacliP fchf\ tfro prograra nairis i& on
the list of iGgljjircaiVe proof jstepa, and, jf so, cjp^rat^s t;]i^ pro-
eraoii ?ha ri:Suli; irKj3.T;:tes whether or not the step was o/orreit;
the proof tU-.p pro&rara ]]andlen the up^citir^ th*it needa t-o be done.-
-IS-
.
T]i3 Method ProfTafn
Wet hod 1? called iipon repeatedly by Verify tc furnish pre of
steps.. IfJhlle Verify will prob&bly reirj.ln unfihin^d £S the Proof -
oheclcer is piodHfiefl, itat'.-ujd iciii be highly rubiest to chants.
Method us as hecriatj.c isathods, in general, to determine what the
next proof atop should be. At present, Hetfrod air.rjly feed* the .
Input directly tc Verify, but this is onijr in order to check out
Vsrify, As wrar-k progresses * Kathod will bscoBia ttore and Lr L o?e
elaborate ,
Qna possible way of elaborating Method it to 3o to hierar-
ofri^ally, R^thsi 1 then reh"?5.t£ Ketlt?i tc acoounfc for hsw lnprow-
casnts* t new Method would by written which uses the ojd ons as a
subpposrrii?. This technique is well adapted %a heuristic progparas.
F tela of Condon g u'o g* pr J s 3 i_or g
In eucesseiv* sufficienc-is^ there will often be Urge sub-
expr&SBio:rjE which &*£■ carried elc-ng intact and er j j therefore
idsnticalr The Proofcheo'icer ha? b^en tr girt:, zed £o aa to have both
sufficiencies refer to fcha sai*i2 ropy ^f such a subexpression. In
gonRral, copying is t^oidil as much a» possible, stvlns storage
and time*
Tuis might appear to bs merely a pracsirjai programming device t
but it has an interact ins counterpart In ta;^booV cia the mat led .
Ea^antially, ccrarson pubeipraoetons not like pron.o^inc; thny are
useful in the sajoe way that it is useful in a boo.c to write an
equation, nurab=r it, ana later on refer to i.t by number. If mo
did not use the numbering techniqje op its equivalent, rfe would
have to write the equf-tion out in fun whenaTsr we wanted to refer
to it.
•
-13-
LOGlCftL FOljmtfiTKHS OF TEE PR
Vs will etart with £ siaes or pairs ^j*^) for * = £/ £ # - - i
which we shall call Iftifrlal tLeargflg » K&eh T i is a ayutoolic «.-
preE£lon;ea<:b B^ is a £«t af at^TJ-fl Eymtols ctr^Mia* l "* '^In J
V* refer to ^ &i? th? fcjriL of ttiie theorem arrt to '.hec^, as the
vs .frii.tles of the thsoran*. .tf jj ^ P ■_ 2 P *♦- r u-^ are eyrc-boli-i ex-
pi-ei»t:ionp, than the result of putytitJting ^^ for^i^u^ for ^g*
,.• , u ]c forct^j, Jn ^ iB a theorem i nat&nge . Kt-i L e that the T^
■ k
are thtiorera- ine-Kinces ty the jfl^n-ifcy substitution.
A proper tyl^cs gyaftol is att sialic symbol l?hl£t is used solely
sr a variable in a theo-rer, and for no o-'her purpose, For inatancft,
&10 and PSAISE woxld not be proftrfcylese symbols* In LIS?, the
function GEK3YM In used tc triage these symbols.
Ie~ 5_ bs a symbolic axprc&n? on, and HippofiQ 1:hafc there exists
a fl^juenoe of sent elites S,, 3 2 , -,• , S n F-^ch that 5^ — S 4 /;. = 1 ,
2. , -. , n) and ^ is the eyntol ,: T'\ (The neonlng of *-* will be
explain .2d shortly; T reprttents troth.) Ish p^PU, •>« > & m be *
fli:t of prop«rt^lee£ sy^jole, tnd danote thlG set ty^. Than 1 ha
p^lr i&-, r V) i- a nLeorem P-jrthsrn^re^ the initial theorems are
theoz-nin;- * The class of thsoz'eire if tKjs forced recursively,
tarring with the initial theorems.
We 6eaot,& "i" ia a trhsorent inKs^e' 1 by - s.« an J tt it is
sufficient to pro re P'" ty *"J 3., The logical ays'eni IB baRfcd on *:wq:
riles of Inference*
1. If h T and -t S, then -i T"iS. f Insertion rale)
3, If t-5^5 1 and -fS*,, Mien H?. (Modus, ponens )
■
- A - ■
jnt.-'j.it^ftjy* £ ~- F [ m*ann -f S ^ -/P 1 . Formally tte say
S,«- S [ if and onlj- if
■" - L S ! lis of the form Tr*. 1 ? and f- T, fir
•:.«-. E, /* S l :??, or
J, S' 1b obtained froTi S by substituting for foms eabex-
prappion of S the equl-Yr,lsnt of that &jb express ion, provided that
the auto evp re Eaton la ; L *ot part cf a quoted eubejcpreasion,
Eo^ vacant subexpressions are of twa types;
1* ft def Inad tenn la 5 qui v slant to thai; Khith It def< naa«
£« An exproaeioii i.;hich r spree gli^ tha raeaiL: of a calculation
IP eq\A5, volant to the : ii e&ult itself." Fhe calculation ie p9rfoi*Ji£d
F;y evaluating the expression ajad then replacing it by the quoted
reauit of the eva^uat^on.
For instance,
ttoiQd be equivalent to
(QUOTE, £CGH3, (?, [A, B)})*
Here £UB#T 1e a LIS? function which sjh6titu*:ss its first EirfciM&nS
for Itc second ar^upgnt :ln lb 9 third argura-irit r
1:he lefinltior; of — 3 a .? hanged vjberi, mfrtatlisarsTrE are .added to
^h<j sjietufj-i Eherafcre, ;he above description corresponds to the
»y&feera arc it now s^a-i^da, but in ry»t perifoarxiRC T
Role cf Initial T'.^'sorece
■■■Tie initial theorems differ from ejeioras as we think of thew
In thfifc Cor H^st preplan, detains fchere is no effort to snake t-hei.i
non-rodu^dint ^ By ual^g a system wjtli a lar^e initial endowment,
iri;.ej?rj5t!.ng result: 1, sra raa/hed more c nicely. It Is true that all
of esa'jhe natlca may bis constructed from lower predicate calculnc
with identity; bat the working Gathe3tf.ti.cian clcss not ordinarily
ral^e lee of bills fiLf;t, even tho^n he la aware of it* This is as
true -."or t^po„ogla.bs arid algebralaleU. as it is for hyvSrodyr^mi^iet*
ar.1 nimri-ml analysts, even though the former may occasionally give
This page is
missing from
the original
document.
-16-
h,; he Varmnt of the? Calc ilstl^n R^e
In psr-crj.UUiR t*e cuictij atiari r-.il 9 r we have 1st the wolf in
the door. Wo voulA life trhs Froof^haslcer, when g*ven a proof, to
te fuarfikTitaed to ^.vt? ui ft vordiit- However, whan wo j.hfcrodus*
t-hfe G&lGUl&tiior! r-:;.e, t--J cefl. rto ledger guarantee this, except at
great coE-t. FG* whsm w-i ceietrt acme gutsxpreaaion of the sufficiency
ar^ci proceed to da:- f-iilct a iia v&lu*, fcii& ealiiiliitlori ir-ay rot ter-
crtiAte; furthermore p U f.B in ffjrt'rAl '.K^r»e?ibl^ it protest the
sut express ion to see ^hethir r-r r.ol liie eal^ulafclcn t.ill r-n wild
?r: aors X&T.B& art;? d^f/fr^ t'-.t; Proof r^n^e* 1 prc-gratf or r,c?Jify its
sonkents , {A fantastically ^lcvar j.aarj:ir<£ prcsraw, for infrtante,
iiwcht ie;irn to eh*iat by tnodifylng she p&rai&iesGrs of the Proof -
-he-L^er do &? tc Tot'-s i'r to asso^ fal r .s ^epai; J iho»-i problem
may be skived by running all s&I-rolatleK steps «i fin Interpretive
b'arSs, bat this requires a yrl /&.te and <juite elaboraU interr*eisr
Per tke ?roofchca;jst»j fu^tl«eru!ore, it w^uld be jJHfco&Fa£ly !rip*e*-
consuming because i3B.ahin.*-i&ng , 'irLfre progrSiaE at t*&l^ EJ9 higher-
^e*'5;i-- ! a:'j ( g-j££ J r£ J ' praj.;:^^ '-.oiiid h£"t; te bo interpreted
r ?hi:* diffiri-jity la ;-:&r*died by placing ail calculations imdor
the control ^: a program rat'ert Errorccr... Errn^et causes meat;
detected errwffts and .'.orj- ! eppiJnatli^ c&ic-jiatieh* to return to con-
trol to 1 -ha Fx i aafiihettfc'7r . It raili net £?it-V(i an pu;:t, arrorf*; so
;h:l.g loslstl jLoapbaln do?? rsrta:n, Eowysr, defective proofs Khlah
do get by Error 35 1 tflil ardi nar3 iy c£P5& Hie ?»&■*> fuhtM^er to 6 top
richer t^an to ?£v-5 & fa~'?.3 ail^Y^r.
■i;-
TSSJ& POCKVX-Iii S'ltFS IS Tii'i raOOFCilHSTJES
Wrien Verify rs^e-Sv^s a proof step flora Method, it checks to
sea if th* step Ss of on? c? th& rsict|."C«^ tvt , ^i J &^G has the
appropriate svitfr-er of parage 1 , ctt ^li:-h 5 t . If" rat , *he step *e
erron'aaus, If thece ?:i3tai*ia a?a j&ef;, t > : & ti^re o:* Vr-.c i:-,ep ie
fasten as the r.^irt of ft fjan£iJLcn, a.nd Mna pir&iT^t&PS of the c,:&p as
avgiunsjnt? Pf U-.^t Fuiw.fclott- fot- ei! , >r hypo of step f she jorKv-
Erp^hdlRg F'.ino 4 '* on LV}ic-. n it? the !?-tcu ».c foe i.f f it \G .■ , :0.. , ?'3.;t Ahd, ii
£lv, £■?-£;■ tha jw-s^ssery updating 1'r c function i? tfuleti by Verify,.
The typas of prf.rf ^tspF have tet.'?. e <j Ler.teci fer rJie.'.r uris-
fulness a? pf!miri<;ot : - or* bit-LId^ng-blc^lts is coiiatfjtfv.ifijv T-he r:yp*:£
of r 4 . sp* w are rea.^y 5 1*^ row ted ift. Th*? £*$; r&ol all ueefa2 by
fr.be pp a?, vet? . t*- v, eve _*■ , v> ; « -, ^. & i i xi £ l-c jpr a .id -lX; fcfc 3 n i d hI tl: r^e r ta I ft
ffpa?4flr theoreiffi, rtty bj'jol-5 =jui":E ptf-tsrilll.
The- fc;:ir>tffa# step.* art a¥ai}.B*Xa a* freyeut;
tiii ti pl'ep lass a? par sine ?>arc She n&ws of -a theorem
and a 1 5 k i r.f p i A h t *. ? i* c i c na . T he c or \ ■■& s po r*3 ! ng f utu* ti o^
finds t>>e theorea on the theorem D.J'-S - . perfc-rras. the i
ind icat e d ?, abn i i t u£ i t n"? . and t h en app 15 m t ! "ii - ^r a v t if: r,
suie io the resulting. xhaor*i3 lr.jnan:o a^»1 tfca curr^n;;
ft uf fide-nay. if tha n?ise(3 tb&orein r,s wo 5 on the* thsoren
Ii.et, or if th«; variatifts r .r- fciw etiibstlt it'^cri r-i*'t do
not corre^-jO'M ' z.- t'cs :^r- i*5j.s:.. c? X'r.s C'.eotcin, the step
is redacted,
l^^s e^^p h£.a t." parameter tin-. naiEa of s theorem*
The correspcnii^JiE f^msticn flr.-i^ tl-.e Theorem on &hs
thaorais li-ft, ^etermjnea iht px-npei EJbititutiOTW for
th& Var^sait'S tf tl*e L^eorena,, p.n:l v ,h.?i sppii^s ttj& r^it
of r'ttt'BrAB -ipiup ponena i-o t?ie ;'-e iUlt ;.n^ theorsrn ard the
i ui re n f, & ■. if f i .4 :: eh; j? k Th ^ ■-- \ & x ■■ -.-■ \. i ;-. b:» ?v- jes t=ed If 1 1 o
nutae'd ^n?orere ;' ■? nor f^n :i e '^-eoresr. H?t, cr if t.!i* ther-.^
rtf-
t/.r. nat c.f the f'pr.i (Ih'ME?, antecedent, eonsffrijent 3 , or
If She sufficiency "* no* a fi Jibuti tut ion i*istan.%e of the'
nonsequent with reject to tha varieties of '-he theorem .
■?hla step faa a* arg'itier.fc & lt*t cT A's art4 D ; a tfMsfc
indicate the. a ufc s K.pr e * rr .1 en of fcfro c i-f t* J - c lc *>;* y ft her e va > ije
is to be calc^atsS. If the i;.Fb Y.&h r,o alMfehia, the
F'jbexprefisiori is the entirs entprsfcsicn* T^ie rt-?p rap"ia*i»G
the nubexprevfiScin * ty Li at (QHCTE; #val[/]l* The &fcep
will be re Jet to-:! if the list reaches nu ascitic symbol c>i H
a quoted exprtt-sicr, po?c;'<» :; ^ &\hi;-;y ;.<M .
Mr.is step hat af- QrjTMLnjiit^ & na-^ r a 1'tl of ■,■ ariaV Isj ±
and a form. »?i th.f. =s ?^pp T t.'oe ?roc^cher-.ker in used
recuPfi'velTj £o eh^u the proof of a lemgta, ahil? ^ erupt -
rarily neglecting L.fce? main tr^crem, XV rhe APin^a ia
proven ; it le added to the zfczor&u list; in eny caae T t oc-
troi 1? ret-iFTW!- to the prccf of '.he Ttsain theorstf wh*f:
either the ieaac-s ia proven or th? r -r oof ghee !/er ia is 16 to
giv* y$j m it,
5, M&kedEf
Thi.3 Siep haa as ar^Juanttt a nams, a list of variables,
an^ a for©. The sorrespenaing fono#ion firs', assign? an
interna^ nzuae to be th-3 equivalent or the TT& France ri£it:e.
It then pla.ics the list which contalna bo^.h nsnsss, the
variables, , ejfot the for** at tr.e begjLnnin,^ of U"j*s tff fir,' t:. Oil
116 1-
Thir. Siiftp Ivf.i* af parsmster^ s, r.anrs ani a Hit- of A -a
ani D'ji„ Ths A l 4 F4^ D's ar£ ur.e:l r,o indicate a Ruhej.-
pref.ft5.on of the &uf£loIejrKj7: the name ^a Vhe re f trance
narje «r a i^firjl.tior, . ?'!"■«■ a-orre^j^nii^^ ^unotien ^e^i
i!e 3e'fir.it1rs:i frnm J-.h? i*firj;icn ii*v a^.? cha^ir t-.ft*
■j-.ilr-exTjref'.sicri to ree if i. :3^ & iat:-;it,jtion intt.pr.-fl of
19
the fann of the de fin iti on< It 1 ?"^ it t-c-;-j ;i;aa sh* sut-
ejpression by ti llss nfoose first alftjaar^ i« rhe interna'-
narao- of the definite ce, ?h^ remitting elements haire the
property that ;,f thoy are maiihed sequentially with the
variables or ?.he difinlfc'on ami nuLft<u&M for ther*e
variables 1'^ the forw, the result Ifl the original
subexpression..
T* yn-Je f * no
Th', P E-.op hf.k as paries!;, er a 11 it cnf A F E anl r c &
Hhigh indicate e. sutcjipres^^rj of the ciffieiefisy* The
first el^Btar-fc of this :i:;!l.e:':p:r5B'iiar[ i^ t&'Ken a# the !/■-
terra! nacre o" a defini titn, an;t che definition list is
bsarehed for ^at naore. a oatatAsution llFt* is fora,-?d
by na tubing thf- euacesaive alercents of Bhe subexpression
with T-bs v£riabze:i cf the definition^ an 2 then the
indioal-ed a , jfcst,s.t ation* ors performed on tbo forra of th-j
definition,. P:.nally J the 5 Un Repression \c. replaced by
the result of this substitution. Ehe step is Fixated
if the naKe^l d^fiuitioa i* not &n the definition list,
or if the number =f e!i agents foMo^'.rj^ the internal name
of She "tef'n.V^ott in 1-ht ^-iiic-yp:e j >fien Ts-nat a^ual to
the njr.ibor of \&.rifctlt:3 ci' r^ euberpre salon.
Th; 1 -j **>ep haE af ^r;; no '. 5T & reference naine . It
causes *-: pair fhees fi?rt oleisent is, the na-w and Nftose
Teccrrf els-^n', i* t?.«e a arrant- sufficiency to le pla^d an
the list of prefe-srved JEUVprfltlCMl, The aurrent BaffieietK?
wll] he- aMe to be itohvOt-.sj .Vf n^i e^E^ry a 1 ; a later tiTis-.
9. fiea t_t!i^;j![
"h.^s step has a?, parameter ttie raraa of a 5 ^bprofclera
on ih« lis? of preserved &ubpret lecig- ■ X~ causes the
current auff'iclensy to te ->et to tbe- & L jf fiaien^y psire-3
-20-
wlth bhe gi.vari nana on (h* Ms 1, of prt'atrvecl nu^praMeas..
Eh? Etep is r£js<i:^c-rl XT the naius <5ois imt cor-Fo-spojvl ic a
Tiiia ;jf.?p har- at pa 7 ir,:c-l,ei" the iniue of a prokl?m 01;
the list of prefer ved su'.-prfti.leJHS . ICt ea;j.£i?£ that s-Jb-
pjroblem tD bs csje'ied frcr- the Iijt v
11, jp-j nath^ g
^riift Et;en has nc parsi^ters, .and has ito effect
fchatsotrer h
IE. geygrt
?b*p r.i ep ha^ nfl parar.L aer*£ . It cfcUf.en as to take
tir.fr aer-OMi nott recent. &uff,1.( J.-e.r;Cy a*? thy Current
eufficiewy* If tte ruirent sufficiency if the theorem
we wish tr prove, Uj-> step If.-. itst j^steeK Ifoleis the current
&ufflcisrjjj it? sived ty a riE.mepr>: f a revert trill C2 l ^-e it
to be Loefci
*£hi& ?iie|i has n^ par&rae^erft. ."Lf the ejrrsnfc s.tfflfi&n^y
1e "T", u* place the th&wea .if, the It's* A of the theorem
llstj Rnd Voril'y will return with Lrt ans"*? of Ti If tihe
eufflalenoy 3p r^t- 7 r t-hfc s-.ep 2 s rejected.
...
&&&E3¥2 STATUS WD FBT-JRJ; PLA'W
: -^'-i
llf of this writing, the Verify p-rot.ran is In the process a J'
debugging, and the- PfeShod program i* in ifce ime' riwli merit ary fornj
. Kethnd merely tfekes a List of alepe, peel* them off one by one,
and pfifses than to Verify, while print irig o^i; useful lnfonEition.
the ppogrram has teen co3#3 entirely ir: MSF, which seems to te
well suited (re the appjieaMon. Jr: pi&irtirtii&r, ifca handling of
i^otaaon subesprep^onp without raneiie&s&r; dupi* cation will probably
ease the storage difficulties .lonaideraLly when the praMava get
nk^re complicated and the t-rieor;^ &rA definition lists £a^ longer,
ji have already wriev-er. all the functiona which eheok trie differ*: sit.
ftepL', though - c :cne cf t iir-n sr;; in <jee3 c f revision,
After Verify fcJ 3 its satellite functions have bse.ii chs.--ked
o'j^ .1 paan Tic wcrW 02: improving Re«hod, at the same tiins applying
It to ehsrtra^t. aisahrii,. Ky fi^s', c'.e-. will be t-c incorporate
nstiiro-Fteps which Hi. 11 ccrnHne several infiivJducJ atepe along with
gpeniftj ttsQreii^ . ^kr>. t 1 £h-;ll bulla * n sac hi nary i»;hlcb allo^'t
t rjs a "r.e p*j !: £ t e p cine .■;■? m ti a ;?"."- l£ ■ io .1*3 ^.y ill ve n> *-f or "1 np " & jv e ? the £ '.Lb -
Htit-jt.Jona ttJght. he omitted faa 1^ ofler, dotrc ir, ths oi tat ion of a
theorem in a le>. thesis ^ronf}. After that, I shall investigate
various learning itierhi*r.iffiDS whi.?h raij=h^ be incorporated- ' However,
1* ia difficult ta anUsipate a 4 : this point Just what cojra-? the
projsei will foin&w; fh-a plan,* at cash stag* will be infl^en^ed
sr-rsngiy fcy the rOP^Jti* of t-hu pr&ce'3in£ f.taee.
■